interface{-}inr($X$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\lambda$$f$,$s$. $\lambda$$x$.inl (inr $x$ )  o $f$($s$)   o $X$